Nuprl Lemma : d-es_wf
0,22
postcript
pdf
D
:dsys{i:l},
E
:ES{i}. d-es{i:l}(
D
;
E
)
Prop{i''}
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Prop
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
es
is an event system of
D
Lemmas
world
wf
,
fair-fifo
wf
,
possible-world
wf
,
w-es
wf
,
event
system
wf
,
dsys
wf
origin
D:dsys{i:l}, E:ES{i}. d-es{i:l}(D; E) 
Prop{i''} D:dsys{i:l}, E:ES{i}. d-es{i:l}(D; E) Prop{i''} Tx:A. B(x)
x:A. B(x)